i:Id, ds:x:Id fp Type, da:k:Knd fp Type, T:Type, ks:Knd List, upd:update-spec(ds;da),
a:((k:{k:Knd| (k  ks) }State(ds)Valtype(da;k)T)).
"ecl"  dom(ds)
 Normal(T)
 Normal(ds)
 Normal(da)
 (kks. isrcv(k)  i = destination(lnk(k))  Id)
 update-spec-decl(upd;ds)
 ecl-machine2(i;ds;da;"ecl";T;ks;a;upd)
 ||- es.zupdate-spec-vars(upd).
 ||- es.es-decls(es;i;ds  "ecl" : T;da)
 ||- es. vartype(i;z)  ds(z)
 ||- es. & e@i.
 ||- es. & e'e.(z after e')
 ||- es. & e'e.=
 ||- es. & e'e.es-trans-state-from{i:l}(es;ks;
 ||- es. & e'e.es-trans-state-from{i:l}(k,s,v,z'. list_accum(z',nf.nf/n,f.
 ||- es. & e'e.es-trans-state-from{i:l}(k,s,v,z'. list_accum(z',nf.if a(n,k,s,v,s("ecl"))
 ||- es. & e'e.es-trans-state-from{i:l}(k,s,v,z'. list_accum(z',nf.if f(s,v)
 ||- es. & e'e.es-trans-state-from{i:l}(k,s,v,z'. list_accum(z',nf.else z' fi;
 ||- es. & e'e.es-trans-state-from{i:l}(k,s,v,z'. list_accum(z';
 ||- es. & e'e.es-trans-state-from{i:l}(k,s,v,z'. list_accum(upd(<k,z>)?nil);z when e;e;e')
 ||- es. & e'e. ds(z) 

latex

Definitions

x:A. B(x), Id, P  Q, "$x", t  T, Prop, x. t(x), xL. P(x), SQType(T), {T}, x,y. t(x;y), State(ds), if b t else f fi, f(x)?z, 1of(t), 2of(t), Top, true, false, A & B, e@i. P(e), e'e.P(e'), P  Q, Valtype(da;k), x(s), A, update-spec-decl(upd;ds), P  Q, P  Q, P & Q, False, x(s1,s2), update-spec(ds;da), , Unit, Knd, Dec(P), , ecl-machine2(i;ds;da;x;T;ks;a;upd)

Lemmas

update-spec-decl wf, l all wf, Knd wf, assert wf, isrcv wf, Id wf, ldst wf, lnk wf, normal-da wf, normal-ds wf, normal-type wf, not wf, fpf-dom wf, id-deq wf, fpf-trivial-subtype-top, nat wf, l member wf, decl-state wf, ma-valtype wf, bool wf, update-spec wf, fpf wf, R-state-var-rule, fpf-join wf, fpf-single wf, fpf-ap wf, fpf-compatible-join2, fpf-compatible-single-iff, fpf-compatible-singles, Id sq, normal-ds-join, normal-ds-single, update-spec-vars wf, R-all-rule, R-state-var wf, list accum wf, subtype rel dep function, fpf-cap wf, top wf, subtype rel self, fpf-cap-join-subtype, fpf-join-cap-sq, fpf-cap-single, eqof eq btrue, eqtt to assert, iff transitivity, bnot wf, eqff to assert, assert of bnot, es-after wf, es-le-loc, es-vartype wf, es-decls-iff, es-trans-state-from wf, es-loc wf, es-isrcv wf, es-when wf, deq wf, decidable equal Id, R-compat wf, R-state-var-compat3, fpf-compatible-join, fpf-compatible-self